T:Type, R:(TT).
Trans(T;a,b.R(a,b))
 {a, b, c:T. strict_part(x,y.R(x,y);a;b)  R(b,c)  strict_part(x,y.R(x,y);a;c)} 

latex

ProofTree

Definitions	t  T, P & Q, strict_part(x,y.R(x;y);a;b), {T}, x(s1,s2), Trans(T;x,y.E(x;y)), P  Q, , x:A. B(x), A, False
Lemmas	not wf